/****************************************************************************
 * Elisa 1.0                                                                *
 *--------------------------------------------------------------------------*
 * Author: Laurent Granvilliers, Vincent Sorin                              *
 * Copyright (c) 2004 Laboratoire d'Informatique de Nantes Atlantique       *
 *--------------------------------------------------------------------------*
 * Elisa is distributed WITHOUT ANY WARRANTY. Read the associated           *
 * COPYRIGHT file for more details.                                         *
 *--------------------------------------------------------------------------*
 * elisa_interval_test.h                                                    *
 ****************************************************************************/


/**
 * @file elisa_interval_test.h
 * @brief Interval constraint satisfaction for real constraints
 */


#ifndef _ELISA_INTERVAL_TEST_H
#define _ELISA_INTERVAL_TEST_H

#include <vector>
#include "elisa_defs.h"
#include "elisa_constraint.h"
#include "elisa_real_constraint.h"
#include "elisa_interval_form.h"
#include "elisa_interval.h"
#include <algorithm>

NAMESPACE_ELISA
/**
 * @ingroup Interval
 * @class RealConstraintRelationRep
 * @brief Base class for interval constraint satisfaction
 */
class RealConstraintRelationRep : public ConstraintRelationRep
{
public:
	/**
 	 * Constructor
 	 */
	RealConstraintRelationRep ()
	{
	}

	/**
 	 * Destructor
 	 * @post all intervalForm have been deleted
 	 */
	virtual ~RealConstraintRelationRep ()
	{
		for (unsigned int i = 0; i < _eval.size(); ++i) {
			delete _eval[i];
		}
	}

	/**
 	 * Insertion of an interval form in the last position
 	 * @param f the IntervalForm to add
 	 */
	void addForm(IntervalForm *f)
	{
		_eval.push_back(f);
	}

	/**
 	 * Must be called once before lazy evaluation
 	 * Each sub-term evaluation is saved at the corresponding node
 	 */
	virtual void testForward() const = 0;

	/**
 	 * Propagate the contraction of the root node to the children
 	 * @return true if the no inconsistance
 	 */
	virtual bool propagBackward() = 0;

	/*
 	 * Test using the possibly interpretation and the lastly computed
 	 * interval evaluations of expressions
 	 */
	virtual bool possibleValue() const = 0;

	/*
 	 * Test using the certainly interpretation and the lastly computed
 	 * interval evaluations of expressions
 	 */
	virtual bool certainValue() const = 0;

	/// @name Test using the possibly interpretation
	//@{

	/**
 	 * Test over the current box
 	 * @return true if the constraint if possibly satisfied
 	 */
	virtual bool isPossiblySatisfied() const = 0;

	/**
 	 * Test over b
 	 * @return true if the constraint if possibly satisfied
 	 */
	virtual bool isPossiblySatisfied(Box *b) const = 0;

	/**
 	 * Test over the current box using lazy interval evaluation
 	 * @return true if the constraint if possibly satisfied
 	 */
	virtual bool isPossiblySatisfied(const RealVarImpl & v) const = 0;
	//@}

	/// @name Test using the certainly interpretation
	//@{
	/**
 	 * Test over the current box
 	 * @return true if the constraint if certainly satisfied
 	 */
	virtual bool isCertainlySatisfied() const = 0;

	/**
 	 * Test over b
 	 * @return true if the constraint if certainly satisfied
 	 */
	virtual bool isCertainlySatisfied(Box *b) const = 0;

	/**
 	 * Test over the current box using lazy interval evaluation
 	 * @return true if the constraint if certainly satisfied
 	 */
	virtual bool isCertainlySatisfied(const RealVarImpl & v) const = 0;
	//@}

	// protected:
public:
	// @var vector of interval forms
	std::vector<IntervalForm *> _eval;
};


/**
 * @ingroup Interval
 * @class RealConstraintRelationRepEq
 * @brief Base class for interval constraint satisfaction of equations
 */
class RealConstraintRelationRepEq : public RealConstraintRelationRep {
public:
	/**
 	 * Constructor
 	 * @param l the left expression of the constraint
 	 * @param r the right expression of the constraint
 	 */
	RealConstraintRelationRepEq (IntervalForm *l,
	                             IntervalForm *r)
	{
		addForm(l);
		addForm(r);
	}

	/**
 	 * Destructor
 	 */
	~RealConstraintRelationRepEq ()
	{
	}

	/// Access to interval forms
	//@{
	IntervalForm *left()
	{
		return _eval[0];
	}

	IntervalForm *const_left() const
	{
		return _eval[0];
	}

	IntervalForm *right()
	{
		return _eval[1];
	}

	IntervalForm *const_right() const
	{
		return _eval[1];
	}
	//@}

	/// @name Base class's virtual methods
	//@{
	bool isPossiblySatisfied() const
	{
		return const_left()->eval().isPossiblyEqual(const_right()->eval());
	}

	bool isPossiblySatisfied(Box *b) const
	{
		return const_left()->eval(b).isPossiblyEqual(const_right()->eval(b));
	}

	bool isPossiblySatisfied(const RealVarImpl & v) const
	{
		return const_left()->evalLazy(v).isPossiblyEqual(const_right()->evalLazy(v));
	}

	bool isCertainlySatisfied() const
	{
		return const_left()->eval().isCertainlyEqual(const_right()->eval());
	}

	bool isCertainlySatisfied(Box *b) const
	{
		return const_left()->eval(b).isCertainlyEqual(const_right()->eval(b));
	}

	bool isCertainlySatisfied(const RealVarImpl & v) const
	{
		return const_left()->evalLazy(v).isCertainlyEqual(const_right()->evalLazy(v));
	}

	void testForward() const
	{
		const_left()->evalForward();
		const_right()->evalForward();
	}

	bool propagBackward()
	{
		Interval l = const_left()->value();
		Interval r = const_right()->value();
		l.intersect(r);
		return const_left()->propagBackward(l) && const_right()->propagBackward(l);
	}

	bool possibleValue() const
	{
		return const_left()->value().isPossiblyEqual(const_right()->value());
	}


	bool certainValue() const
	{
		return const_left()->value().isCertainlyEqual(const_right()->value());
	}
	//@}

	IntervalForm *_right;
	IntervalForm *_left;
};




/**
 * @ingroup Interval
 * @class RealConstraintRelationRepInf
 * @brief Base class for interval constraint satisfaction of inequalities <=
 */
class RealConstraintRelationRepInf : public RealConstraintRelationRep
{
public:
	/**
 	 * Constructor
 	 * @param l the left expression of the constraint
 	 * @param r the right expression of the constraint
 	 */
	RealConstraintRelationRepInf (IntervalForm *l,
	                              IntervalForm *r)
	{
		addForm(l);
		addForm(r);
	}

	/**
 	 * Destructor
 	 */
	~RealConstraintRelationRepInf ()
	{
	}

	/// Access to interval forms
	//@{
	IntervalForm *left()
	{
		return _eval[0];
	}

	IntervalForm *const_left() const
	{
		return _eval[0];
	}

	IntervalForm *right()
	{
		return _eval[1];
	}

	IntervalForm *const_right() const
	{
		return _eval[1];
	}
	//@}

	/// @name Base class's virtual methods
	//@{
	bool isPossiblySatisfied() const
	{
		return const_left()->eval().isPossiblyLessThan(const_right()->eval());
	}

	bool isPossiblySatisfied(Box *b) const
	{
		return const_left()->eval(b).isPossiblyLessThan(const_right()->eval(b));
	}

	bool isPossiblySatisfied(const RealVarImpl & v) const
	{
		return const_left()->evalLazy(v).isPossiblyLessThan(const_right()->evalLazy(v));
	}

	bool isCertainlySatisfied() const
	{
		return const_left()->eval().isCertainlyLessThan(const_right()->eval());
	}

	bool isCertainlySatisfied(Box *b) const
	{
		return const_left()->eval(b).isCertainlyLessThan(const_right()->eval(b));
	}

	bool isCertainlySatisfied(const RealVarImpl & v) const
	{
		return const_left()->evalLazy(v).isCertainlyLessThan(const_right()->evalLazy(v));
	}

	void testForward() const
	{
		const_left()->evalForward();
		const_right()->evalForward();
	}

	bool propagBackward()
	{
		Interval l(const_left()->value().inf(), 
			std::min<Interval::Bound>( const_left()->value().sup(), const_right()->value().sup()) );
		Interval r(std::max<Interval::Bound>(const_left()->value().inf(), const_right()->value().inf()), 
			const_right()->value().sup() );
		return const_left()->propagBackward(l) && const_right()->propagBackward(r);
	}


	bool possibleValue() const
	{
		return const_left()->value().isPossiblyLessThan(const_right()->value());
	}


	bool certainValue() const
	{
		return const_left()->value().isCertainlyLessThan(const_right()->value());
	}
	//@}
};


/**
 * @ingroup Interval
 * @class RealConstraintRelationRepSup
 * @brief Base class for interval constraint satisfaction for inequalities >=
 */
class RealConstraintRelationRepSup : public RealConstraintRelationRep {
public:
	/**
 	 * Constructor
 	 * @param l the left expression of the constraint
 	 * @param r the right expression of the constraint
 	 */
	RealConstraintRelationRepSup (IntervalForm *l,
	                              IntervalForm *r)
	{
		addForm(l);
		addForm(r);
	}

	/**
 	 * Destructor
 	 */
	~RealConstraintRelationRepSup ()
	{
	}

	/// Access to interval forms
	//@{
	IntervalForm *left()
	{
		return _eval[0];
	}

	IntervalForm *const_left() const
	{
		return _eval[0];
	}

	IntervalForm *right()
	{
		return _eval[1];
	}

	IntervalForm *const_right() const
	{
		return _eval[1];
	}
	//@}

	/// @name Base class's virtual methods
	//@{
	bool isPossiblySatisfied() const
	{
		return const_right()->eval().isPossiblyLessThan(const_left()->eval());
	}

	bool isPossiblySatisfied(Box *b) const
	{
		return const_right()->eval(b).isPossiblyLessThan(const_left()->eval(b));
	}

	bool isPossiblySatisfied(const RealVarImpl & v) const
	{
		return const_right()->evalLazy(v).isPossiblyLessThan(const_left()->evalLazy(v));
	}

	bool isCertainlySatisfied() const
	{
		return const_right()->eval().isCertainlyLessThan(const_left()->eval());
	}

	bool isCertainlySatisfied(Box *b) const
	{
		return const_right()->eval(b).isCertainlyLessThan(const_left()->eval(b));
	}

	bool isCertainlySatisfied(const RealVarImpl & v) const
	{
		return const_right()->evalLazy(v).isCertainlyLessThan(const_left()->evalLazy(v));
	}

	void testForward() const
	{
		const_left()->evalForward();
		const_right()->evalForward();
	}

	bool propagBackward()
	{
		Interval l(std::max<Interval::Bound>( const_left()->value().inf(), const_right()->value().inf()), 
			const_left()->value().sup() );
		Interval r(const_right()->value().inf(), 
			std::min<Interval::Bound>( const_left()->value().sup(), const_right()->value().sup()) );
		return const_left()->propagBackward(l) && const_right()->propagBackward(r);
	}


	bool possibleValue() const
	{
		return const_right()->value().isPossiblyLessThan(const_left()->value());
	}


	bool certainValue() const
	{
		return const_right()->value().isCertainlyLessThan(const_left()->value());
	}
	//@}
};

/**
 * @ingroup Interval
 * @class IntervalTestVisitor
 * @brief Visitor of real constraints used to create
 * an interval constraint satisfaction test
 */
class IntervalTestVisitor : public RealConstraintVisitor
{
public:
	/**
 	 * Constructor
 	 * @param cons Factory for interval form
 	 * @param v RealVarImplementation used for lazy evaluation
 	 */
	IntervalTestVisitor (IntervalFormFactory *createForm,
	                     const RealVarImpl *v)
	{
		_createForm = createForm;
		_v = v;
	}

	/**
 	 * Destructor
 	 * @post cons is not deleted
 	 */
	~IntervalTestVisitor ()
	{
	}

	/**
 	 * Return the computed interval test
 	 */
	RealConstraintRelationRep *rep() const
	{
		return _rep;
	}

	/// @name Base class's virtual methods
	//@{
	void visit(RealConstraintRep & c)
	{
		c.visit(*this);
	}

	void visited(RealConstraintRepEq & c)
	{
		_rep = new RealConstraintRelationRepEq(_createForm->create(c.const_left(), _v),
		                                       _createForm->create(c.const_right(), _v));
	}

	void visited(RealConstraintRepInf & c)
	{
		_rep = new RealConstraintRelationRepInf(_createForm->create(c.const_left(), _v),
		                                        _createForm->create(c.const_right(), _v));
	}

	void visited(RealConstraintRepSup & c)
	{
		_rep = new RealConstraintRelationRepSup(_createForm->create(c.const_left(), _v),
		                                        _createForm->create(c.const_right(), _v));
	}
	//@}

private:
	// @var constructor of interval form
	IntervalFormFactory *_createForm;

	// @var variable used for lazy evaluation
	const RealVarImpl *_v;

	// @var the computed interval test
	RealConstraintRelationRep *_rep;
};

/**
 * @ingroup Constraint
 * @class RealConstraintRelation
 * @brief Real constraint using interval evaluation
 */
class RealConstraintRelation : public ConstraintRelation 
{
public:
	/**
 	 * Constructor
 	 * @param c the constraint to evaluate
 	 * @param cons the factory for the interval form
 	 * @param v the variable used for lazy evaluations
 	 */
	RealConstraintRelation (RealConstraint *c,
	                        IntervalFormFactory *cons,
	                        RealVarImpl *v = 0)
	{
		_c = c;
		if (v == 0) {
			_v = static_cast<RealVarImpl *>(c->beginVar()->get());
		} else {
			_v = v;
		}

		IntervalTestVisitor visitor(cons, v);
		visitor.visit(*c->rep());
		_rep = visitor.rep();
	}

	/**
 	 * Destructor
 	 * @post the factory cons is not deleted
 	 */
	~RealConstraintRelation ()
	{
	}

	/// @name Base class's virtual methods
	//@{

	bool isPossiblySatisfied(Box *b) const
	{
		return _rep->isPossiblySatisfied(b);
	}


	bool isCertainlySatisfied(Box *b) const
	{
		return _rep->isCertainlySatisfied(b);
	}


	void print(std::ostream & os) const
	{
		_c->print(os);
	}
	//@}


	/// @name Lazy satisfaction tests
	//@{

	/**
 	 * Must be called once before a sequence of tests using
 	 * isPossiblySatisfied(v) or isCertainlySatisfied(v)
 	 */
	void initSatisfaction()
	{
		_rep->testForward();
	}

	/**
 	 * ascending evaluation
 	 */
	void evalForward()
	{
		_rep->testForward();
	}

	/**
 	 * backward propagation
 	 */
	bool propagBackward()
	{
		return _rep->propagBackward();
	}

	/**
 	 * Test using the possibly interpretation and the lastly computed
 	 * interval evaluations of expressions
 	 */
	bool possibleValue() const
	{
		return _rep->possibleValue();
	}

	/**
 	 * Test using the certainly interpretation and the lastly computed
 	 * interval evaluations of expressions
 	 */
	bool certainValue() const
	{
		return _rep->certainValue();
	}

	/**
 	 * Test using the possibly interpretation and lazy interval evaluation
 	 */
	bool isPossiblySatisfied(const RealVarImpl & v) const
	{
		return _rep->isPossiblySatisfied(v);
	}

	/**
 	 * Test using the certainly interpretation and lazy interval evaluation
 	 */
	bool isCertainlySatisfied(const RealVarImpl & v) const
	{
		return _rep->isCertainlySatisfied(v);
	}
	//@}

private:
	// @var the associated real constraint
	const RealConstraint *_c;

	// @var the variable used for lazy evaluation
	const RealVarImpl *_v;

public:
	// @var the computable test
	RealConstraintRelationRep *_rep;
};

END_NAMESPACE_ELISA

#endif // ELISA_INTERVAL_TEST
